$\forall$${\it es}$:ES, $A$:Type, $X$:AbsInterface($A$). le($X$) $\in$ AbsInterface(E($X$))